COMMENT ⊗   VALID 00005 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	% use this file for experimental typsetting using th `boo' macros
C00003 00003	% test material goes here
C00017 00004	\end{document}
C00018 00005	% anything can go here as tex won't read beyond the \end{document}
C00019 ENDMK
C⊗;
% use this file for experimental typsetting using th `boo' macros

%  \pagelayout{boo}
\input{boo.plo[b2,jmc]}
%  \documentstyle{boo,boo11}
\input{boo.sty[b2,jmc]}
\input{boo11.sty[b2,jmc]}

\input boomac.tex[b2,jmc]

\nofiles

\begin{document}

% test material goes here

	Lisp is a programming language for computing with the
symbolic expressions that arise in artificial intelligence and
in computation with mathematical formulas.  The core of the
language is called pure Lisp and we begin with that.  Pure
Lisp is most clearly explained rather abstractly.  The data
of Lisp are called S-expressions.

	Begin with a set {\it A} called the set of atoms.  For our
present purpose it doesn't matter what the atoms are.  We only
need to provide a test for equality of two atoms and a predicate
for telling whether an object is an atom.
Because we will need parentheses for Lisp S-expressions,
we use square brackets for applying a function to arguments.
Thus we write $/atom/[x]$ for the assertion that {\it x} is an
atom.  However, we usually reduce the number
of brackets by omitting them for functions of one argument.  Thus
we simply write $/atom/ x$.

	S-expressions are built up from atoms by the following rule.

	{\it An atom is an S-expression, and an ordered pair of
S-expressions is an S-expression.  All S-expressions are formed
in this way.}

	From this abstract point of view we need say nothing about
how S-expressions are represented in the memory of a computer or
on paper.  We do need names for the basic operations on S-expressions.
The operation that forms pairs is called {\it cons}, and we write
$x \qcons y$ for the operation of making a pair out of the S-expressions
{\it x} and {\it y}.

	Inverse to the operation $\qcons$ that forms pairs are the two
operations \qa\ and \qd\ that takes the components of a pair.  These
operations are read {\it car} and {\it cdr} respectively.  The fact
that these operations are inverses is expressed by the equations
%
	$$\qa\ [x\qcons y] = x,$$
%
	$$\qd\ [x\qcons y] = y,$$
%
and
	$$¬/atom/[x] ⊃ [x = [[\qa x] \qcons [\qd x]]].$$

	Here we have used the logical symbol $¬$ meaning {\it not}
and the logical symbol $⊃$ meaning {\it implies}.  We will treat
logical symbolism more fully later.

	We make the the convention that single argument functions
bind more tightly than infixes and relations bind (like equality)
bind more tightly that logical symbols like implication, so the
last equation can be written without brackets as
%
	$$¬/atom/ x ⊃ x = \qa x \qcons \qd x.$$
%
	We need a notation for constant S-expressions.  For the
moment we'll use capital letters for atoms, so that {\sx A},
{\sx B}, etc. denote atoms.  The pairs are formed by surrounding
the paired items by parentheses and separating them with a dot.
Thus {\sx A}, {\sx (A.A)}, {\sx (A.B)} and {\sx ((A.B).(A.(B.C)))}
are all S-expressions.  It is important to distinguish the center dot
operation $\qcons$ that forms S-expressions from
the dot used in writing S-expressions.  The former is an operation
that can be executed, i.e. a program getting {\it x} and {\it y},
computes $x\qcons y$, whatever $x$ and $y$ may be, while {\sx (A.B)}
just denotes that one S-expression.  Of course, we have
%
	$${\sx A}\qcons {\sx B} = |(A.B)|,$$
%
but we can't write $(x.y)$ with {\it x} and {\it y} as variables.

	The fact that the pairs are distinct from atoms is
expressed by the formula
%
	$$¬/atom/[x\qcons y].$$
%
	With what we have so far we can only write trivial facts,
but to check your understanding, notice that the following are
consequences of what we have so far.
%
	$${\sx (B.C)} = \qd{\sx (A.B)}\qcons \qa{\sx (C.D)}.$$
%
	$$/atom/ \qa\qd |(A.(B.C))|.$$
%
	To write pure Lisp programs, we need two more things -
conditional expressions and recursion.

	The expression
%
	$$\qif p \qthen a \qelse b$$
%
is called a {\it conditional expression} and is evaluated as follows:

	First evaluate {\it p}.  If {\it p} is true then the value
of the conditonal expression is that of {\it a}.  Otherwise its
value is that of {\it b}.

	Now we can define a simple pure Lisp program for reversing
the \qa-parts and \qd -parts of an S-expression and its subexpressions.
We'll call our function /flip/, and we want, for example, that
%
	$$/flip/ {\sx ((A.B).C)} = {\sx (C.(B.A))}.$$
%
	The Lisp program is defined by
%
	$$/flip/ x ← \qif \mkop{atom} x \qthen x 
\qelse /flip/ \qd x\qcons /flip/\qa x.$$
%
If you're still shakey on the conventions for omitting brackets, note that
this is equivalent to
%
$$/flip/[x] ← [\qif atom[x] \qthen x \qelse /flip/[\qd[x]]\qcons /flip/[\qa[x]]],$$
%
but from now on the bracket omission conventions will be used without further
explanation.

	The $←$ is means that the left hand side is evaluated by evaluating
the right hand side.  The recursion means that function being defined,
in this case /flip/ may occur on the right hand side (but with different
arguments if the evaluation is to succeed).

	For example, we have
%
$$\vbox{\ialign{\hfil$#$ & $ ← #$\hfil\cr
/flip/ |A| & \qif \qat |A| \qthen |A| \qelse /flip/\qd |A|\qcons /flip/\qa |A|\cr
&|A|\cr
}},$$
%
since $\qat |A|$ is true, not reaching (as the lawyers put it) the issue
of what $\qd |A|$ might be.  Clearly {\it flip} applied to any atom will
be just that atom.  In a more complicated case we have
%
$$\vbox{\ialign{\hfil$#$ & $ ← #$\hfil\cr
  /flip/ |(A.(B.C))| & \qif \qat |(A.(B.C))| \qthen |(A.(B.C))|
\qelse /flip/\qd |(A.(B.C))|\qcons /flip/\qa |(A.(B.C))|\cr
&/flip/\qd |(A.(B.C))|\qcons /flip/\qa |(A.(B.C))|\cr
&/flip/|(B.C)|\qcons /flip/ |A|\cr
&[\qif \qat |(B.C)| \qthen |(B.C)| \qelse /flip/\qd |(B.C)|\qcons /flip/\qa |(B.C)|]
\qcons |A|\cr
&[/flip/|C|\qcons /flip/|B|]\qcons |A|\cr
&[|C|\qcons |B|]\qcons |A|\cr
&|(C.B)|\qcons |A|\cr
&|((C.B).A)|\cr
}}$$

	The pure Lisp function definition
%
	$$/subst/[x,y,z] ← \qif /atom/ z \qthen [\qif z=y \qthen x \qelse z]
\qelse /subst/[x,y,\qa z]\qcons /subst/[x,y,\qd z]$$
%
gives the result of substituting the S-expression {\it x} for the
atom {\it y} in the S-expression {\it z}.  For example,
%
	$$subst[|(A.B)|,|C|,|((C.D).C)|] = |(((A.B).D).(A.B))|.$$

	As we shall see in the rest of the first two chapters,
pure Lisp programs of arbitrary power can be constructed by
using already defined functions in the definition of new ones.

	The simple structure of pure Lisp programs, makes it easy to
regard them as formulas of a language of mathematical logic - a
first order language - to use the precise mathematical terminology.
Proofs of the properties of these programs are then straightforward,
and these proofs can even be put into a form in which they can be
checked by a computer program.  Even better, an interactive theorem
prover can simultaneously help construct the proof and check its
correctness.  You are then only responsible for being sure that
what you proved is what you meant and that you didn't sneak in any
false statements as axioms.

	The function $/flip/$ provides a convenient example of proof.

\noindent{\bf Theorem:} $/flip/ /flip/ x = x$.

\noindent{\bf Proof:} Consider the set {\it goodflip}
of S-expressions {\it x} for which the
theorem is true.  Clearly {\it gooodflip} contains all atoms, because if
{\it x} is an atom, $/flip/x = x$, and hence $/flip/ /flip/ x = x$.
Now suppose {\it goodflip} contains the S-expressions {\it x} and
{\it y}.  We have
%
$$\vbox{\ialign{\hfil$#$ & $ ← #$\hfil\cr
/flip//flip/[x\qcons y]&/flip/[\qif /atom/[x\qcons y] \qthen x\qcons y
\qelse /flip/\qd[x\qcons y]\qcons/flip/\qa[x\qcons y]]\cr
&/flip/[/flip/y\qcons/flip/x]\cr
&\qif\qat[/flip/y\qcons/flip/x]\qthen/flip/y\qcons/flip/x
\qelse/flip/\qd[/flip/y\qcons/flip/x]\qcons/flip/\qa[/flip/y\qcons/flip/x]\cr
&/flip//flip x/\qcons/flip//flip/y\cr
&x\qcons y\cr
}},$$
%
which shows that {\it goodflip} also contains $x\qcons y$.  Now look
back at the definition of the set of S-expressions.  It is the
least set that contains all atoms and whenever it contains {\it x}
and {\it y} also contains $x\qcons y$.  Therefore, {\it goodflip}
contains the set of all S-expressions, i.e. the relation
$/flip//flip/ x = x$ is true for all S-expressions {\it x}.

	More interesting properties of computer programs admit similar,
though usually longer, proofs.  However, such informal
proofs are not checkable by computer.  For simple properties like
this, the computer checkable form is much shorter.

	Also this proof glosses over a number of difficulties that
require the more detailed treatment given in Chapter 3.

	This completes our abstract introduction to pure Lisp and
its proof methods.

	S-expressions are convenient for giving the abstract
properties of Lisp, and, as we shall see, they are convenient
to represent in the memory of a computer.  However, for the
representation of most interesting kinds of symbolic information,
lists are more convenient.  We now show how information is represented
by lists and how lists are conveniently represented by S-expressions.
\end{document}
% anything can go here as tex won't read beyond the \end{document}